The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0) → plus_x#1(x3, comp_f_g#1(x1, x2, 0))
comp_f_g#1(plus_x(x3), id, 0) → plus_x#1(x3, 0)
map#2(Nil) → Nil
map#2(Cons(x16, x6)) → Cons(plus_x(x16), map#2(x6))
plus_x#1(0, x6) → x6
plus_x#1(S(x8), x10) → S(plus_x#1(x8, x10))
foldr_f#3(Nil, 0) → 0
foldr_f#3(Cons(x16, x5), x24) → comp_f_g#1(x16, foldr#3(x5), x24)
foldr#3(Nil) → id
foldr#3(Cons(x32, x6)) → comp_f_g(x32, foldr#3(x6))
main(x3) → foldr_f#3(map#2(x3), 0)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0) → plus_x#1(x3, comp_f_g#1(x1, x2, 0)) [1]
comp_f_g#1(plus_x(x3), id, 0) → plus_x#1(x3, 0) [1]
map#2(Nil) → Nil [1]
map#2(Cons(x16, x6)) → Cons(plus_x(x16), map#2(x6)) [1]
plus_x#1(0, x6) → x6 [1]
plus_x#1(S(x8), x10) → S(plus_x#1(x8, x10)) [1]
foldr_f#3(Nil, 0) → 0 [1]
foldr_f#3(Cons(x16, x5), x24) → comp_f_g#1(x16, foldr#3(x5), x24) [1]
foldr#3(Nil) → id [1]
foldr#3(Cons(x32, x6)) → comp_f_g(x32, foldr#3(x6)) [1]
main(x3) → foldr_f#3(map#2(x3), 0) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0) → plus_x#1(x3, comp_f_g#1(x1, x2, 0)) [1]
comp_f_g#1(plus_x(x3), id, 0) → plus_x#1(x3, 0) [1]
map#2(Nil) → Nil [1]
map#2(Cons(x16, x6)) → Cons(plus_x(x16), map#2(x6)) [1]
plus_x#1(0, x6) → x6 [1]
plus_x#1(S(x8), x10) → S(plus_x#1(x8, x10)) [1]
foldr_f#3(Nil, 0) → 0 [1]
foldr_f#3(Cons(x16, x5), x24) → comp_f_g#1(x16, foldr#3(x5), x24) [1]
foldr#3(Nil) → id [1]
foldr#3(Cons(x32, x6)) → comp_f_g(x32, foldr#3(x6)) [1]
main(x3) → foldr_f#3(map#2(x3), 0) [1]

The TRS has the following type information:

comp_f_g#1 :: plus_x:0:S → comp_f_g:id → plus_x:0:S → plus_x:0:S plus_x :: plus_x:0:S → plus_x:0:S comp_f_g :: plus_x:0:S → comp_f_g:id → comp_f_g:id 0 :: plus_x:0:S plus_x#1 :: plus_x:0:S → plus_x:0:S → plus_x:0:S id :: comp_f_g:id map#2 :: Nil:Cons → Nil:Cons Nil :: Nil:Cons Cons :: plus_x:0:S → Nil:Cons → Nil:Cons S :: plus_x:0:S → plus_x:0:S foldr_f#3 :: Nil:Cons → plus_x:0:S → plus_x:0:S foldr#3 :: Nil:Cons → comp_f_g:id main :: Nil:Cons → plus_x:0:S

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

foldr_f#3
main

(c) The following functions are completely defined:

comp_f_g#1
foldr#3
map#2
plus_x#1

Due to the following rules being added:

comp_f_g#1(v0, v1, v2) → 0 [0]
plus_x#1(v0, v1) → 0 [0]

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0) → plus_x#1(x3, comp_f_g#1(x1, x2, 0)) [1] comp_f_g#1(plus_x(x3), id, 0) → plus_x#1(x3, 0) [1] map#2(Nil) → Nil [1] map#2(Cons(x16, x6)) → Cons(plus_x(x16), map#2(x6)) [1] plus_x#1(0, x6) → x6 [1] plus_x#1(S(x8), x10) → S(plus_x#1(x8, x10)) [1] foldr_f#3(Nil, 0) → 0 [1] foldr_f#3(Cons(x16, x5), x24) → comp_f_g#1(x16, foldr#3(x5), x24) [1] foldr#3(Nil) → id [1] foldr#3(Cons(x32, x6)) → comp_f_g(x32, foldr#3(x6)) [1] main(x3) → foldr_f#3(map#2(x3), 0) [1] comp_f_g#1(v0, v1, v2) → 0 [0] plus_x#1(v0, v1) → 0 [0] The TRS has the following type information: comp_f_g#1 :: plus_x:0:S → comp_f_g:id → plus_x:0:S → plus_x:0:S plus_x :: plus_x:0:S → plus_x:0:S comp_f_g :: plus_x:0:S → comp_f_g:id → comp_f_g:id 0 :: plus_x:0:S plus_x#1 :: plus_x:0:S → plus_x:0:S → plus_x:0:S id :: comp_f_g:id map#2 :: Nil:Cons → Nil:Cons Nil :: Nil:Cons Cons :: plus_x:0:S → Nil:Cons → Nil:Cons S :: plus_x:0:S → plus_x:0:S foldr_f#3 :: Nil:Cons → plus_x:0:S → plus_x:0:S foldr#3 :: Nil:Cons → comp_f_g:id main :: Nil:Cons → plus_x:0:S Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: comp_f_g#1(plus_x(x3), comp_f_g(plus_x(x3'), comp_f_g(x1', x2')), 0) → plus_x#1(x3, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) [2] comp_f_g#1(plus_x(x3), comp_f_g(plus_x(x3''), id), 0) → plus_x#1(x3, plus_x#1(x3'', 0)) [2] comp_f_g#1(plus_x(x3), comp_f_g(x1, x2), 0) → plus_x#1(x3, 0) [1] comp_f_g#1(plus_x(x3), id, 0) → plus_x#1(x3, 0) [1] map#2(Nil) → Nil [1] map#2(Cons(x16, x6)) → Cons(plus_x(x16), map#2(x6)) [1] plus_x#1(0, x6) → x6 [1] plus_x#1(S(x8), x10) → S(plus_x#1(x8, x10)) [1] foldr_f#3(Nil, 0) → 0 [1] foldr_f#3(Cons(x16, Nil), x24) → comp_f_g#1(x16, id, x24) [2] foldr_f#3(Cons(x16, Cons(x32', x6')), x24) → comp_f_g#1(x16, comp_f_g(x32', foldr#3(x6')), x24) [2] foldr#3(Nil) → id [1] foldr#3(Cons(x32, x6)) → comp_f_g(x32, foldr#3(x6)) [1] main(Nil) → foldr_f#3(Nil, 0) [2] main(Cons(x16', x6'')) → foldr_f#3(Cons(plus_x(x16'), map#2(x6'')), 0) [2] comp_f_g#1(v0, v1, v2) → 0 [0] plus_x#1(v0, v1) → 0 [0] The TRS has the following type information: comp_f_g#1 :: plus_x:0:S → comp_f_g:id → plus_x:0:S → plus_x:0:S plus_x :: plus_x:0:S → plus_x:0:S comp_f_g :: plus_x:0:S → comp_f_g:id → comp_f_g:id 0 :: plus_x:0:S plus_x#1 :: plus_x:0:S → plus_x:0:S → plus_x:0:S id :: comp_f_g:id map#2 :: Nil:Cons → Nil:Cons Nil :: Nil:Cons Cons :: plus_x:0:S → Nil:Cons → Nil:Cons S :: plus_x:0:S → plus_x:0:S foldr_f#3 :: Nil:Cons → plus_x:0:S → plus_x:0:S foldr#3 :: Nil:Cons → comp_f_g:id main :: Nil:Cons → plus_x:0:S Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
id => 0
Nil => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(x3, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), z = 1 + x3, x3' >= 0, x3 >= 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(x3, plus_x#1(x3'', 0)) :|: z'' = 0, z = 1 + x3, z' = 1 + (1 + x3'') + 0, x3 >= 0, x3'' >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(x3, 0) :|: z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z = 1 + x3, x3 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(x3, 0) :|: z'' = 0, z = 1 + x3, x3 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 0, x24) :|: z = 1 + x16 + 0, x24 >= 0, z' = x24, x16 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), x24) :|: x6' >= 0, x32' >= 0, x24 >= 0, z' = x24, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ x6 :|: z' = x6, x6 >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus_x#1(z, z') -{ 1 }→ 1 + plus_x#1(x8, x10) :|: x8 >= 0, z = 1 + x8, z' = x10, x10 >= 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(z' - 2, 0)) :|: z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 }→ 1 + plus_x#1(z - 1, z') :|: z - 1 >= 0, z' >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ plus_x#1 } { map#2 } { foldr#3 } { comp_f_g#1 } { foldr_f#3 } { main }

(14) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(z' - 2, 0)) :|: z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 }→ 1 + plus_x#1(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {plus_x#1}, {map#2}, {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: plus_x#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(16) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(z' - 2, 0)) :|: z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 }→ 1 + plus_x#1(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {plus_x#1}, {map#2}, {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: ?, size: O(n1) [z + z']

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: plus_x#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(18) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(z' - 2, 0)) :|: z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 }→ plus_x#1(z - 1, 0) :|: z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 }→ 1 + plus_x#1(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {map#2}, {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {map#2}, {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: map#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(22) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {map#2}, {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: ?, size: O(n1) [2·z]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: map#2
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(24) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 2 }→ foldr_f#3(1 + (1 + x16') + map#2(x6''), 0) :|: z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 1 }→ 1 + (1 + x16) + map#2(x6) :|: z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: foldr#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(28) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {foldr#3}, {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: ?, size: O(n1) [z]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: foldr#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(30) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 1 }→ 1 + x32 + foldr#3(x6) :|: z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(x16, 1 + x32' + foldr#3(x6'), z') :|: x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z]

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 3 + x6' }→ comp_f_g#1(x16, 1 + x32' + s5, z') :|: s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: comp_f_g#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(34) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 3 + x6' }→ comp_f_g#1(x16, 1 + x32' + s5, z') :|: s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {comp_f_g#1}, {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: ?, size: O(n1) [z + z']

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: comp_f_g#1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z + z'

(36) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 2 }→ plus_x#1(z - 1, plus_x#1(x3', comp_f_g#1(x1', x2', 0))) :|: z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 3 + x6' }→ comp_f_g#1(x16, 1 + x32' + s5, z') :|: s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 2 }→ comp_f_g#1(z - 1, 0, z') :|: z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z']

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 4 + x1' + x2' + x3' + z }→ s9 :|: s7 >= 0, s7 <= 1 * x1' + 1 * x2', s8 >= 0, s8 <= 1 * x3' + 1 * s7, s9 >= 0, s9 <= 1 * (z - 1) + 1 * s8, z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 + z }→ s10 :|: s10 >= 0, s10 <= 1 * (z - 1) + 1 * 0, z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 5 + s5 + x16 + x32' + x6' }→ s11 :|: s11 >= 0, s11 <= 1 * x16 + 1 * (1 + x32' + s5), s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z']

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: foldr_f#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(40) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 4 + x1' + x2' + x3' + z }→ s9 :|: s7 >= 0, s7 <= 1 * x1' + 1 * x2', s8 >= 0, s8 <= 1 * x3' + 1 * s7, s9 >= 0, s9 <= 1 * (z - 1) + 1 * s8, z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 + z }→ s10 :|: s10 >= 0, s10 <= 1 * (z - 1) + 1 * 0, z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 5 + s5 + x16 + x32' + x6' }→ s11 :|: s11 >= 0, s11 <= 1 * x16 + 1 * (1 + x32' + s5), s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {foldr_f#3}, {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z'] foldr_f#3: runtime: ?, size: O(n1) [z]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: foldr_f#3
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 2·z

(42) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 4 + x1' + x2' + x3' + z }→ s9 :|: s7 >= 0, s7 <= 1 * x1' + 1 * x2', s8 >= 0, s8 <= 1 * x3' + 1 * s7, s9 >= 0, s9 <= 1 * (z - 1) + 1 * s8, z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 + z }→ s10 :|: s10 >= 0, s10 <= 1 * (z - 1) + 1 * 0, z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 5 + s5 + x16 + x32' + x6' }→ s11 :|: s11 >= 0, s11 <= 1 * x16 + 1 * (1 + x32' + s5), s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 2 }→ foldr_f#3(0, 0) :|: z = 0
main(z) -{ 3 + x6'' }→ foldr_f#3(1 + (1 + x16') + s4, 0) :|: s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z'] foldr_f#3: runtime: O(n1) [2 + 2·z], size: O(n1) [z]

(43) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(44) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 4 + x1' + x2' + x3' + z }→ s9 :|: s7 >= 0, s7 <= 1 * x1' + 1 * x2', s8 >= 0, s8 <= 1 * x3' + 1 * s7, s9 >= 0, s9 <= 1 * (z - 1) + 1 * s8, z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 + z }→ s10 :|: s10 >= 0, s10 <= 1 * (z - 1) + 1 * 0, z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 5 + s5 + x16 + x32' + x6' }→ s11 :|: s11 >= 0, s11 <= 1 * x16 + 1 * (1 + x32' + s5), s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 4 }→ s12 :|: s12 >= 0, s12 <= 1 * 0, z = 0
main(z) -{ 9 + 2·s4 + 2·x16' + x6'' }→ s13 :|: s13 >= 0, s13 <= 1 * (1 + (1 + x16') + s4), s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z'] foldr_f#3: runtime: O(n1) [2 + 2·z], size: O(n1) [z]

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: main
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(46) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 4 + x1' + x2' + x3' + z }→ s9 :|: s7 >= 0, s7 <= 1 * x1' + 1 * x2', s8 >= 0, s8 <= 1 * x3' + 1 * s7, s9 >= 0, s9 <= 1 * (z - 1) + 1 * s8, z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 + z }→ s10 :|: s10 >= 0, s10 <= 1 * (z - 1) + 1 * 0, z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 5 + s5 + x16 + x32' + x6' }→ s11 :|: s11 >= 0, s11 <= 1 * x16 + 1 * (1 + x32' + s5), s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 4 }→ s12 :|: s12 >= 0, s12 <= 1 * 0, z = 0
main(z) -{ 9 + 2·s4 + 2·x16' + x6'' }→ s13 :|: s13 >= 0, s13 <= 1 * (1 + (1 + x16') + s4), s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {main}
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z'] foldr_f#3: runtime: O(n1) [2 + 2·z], size: O(n1) [z] main: runtime: ?, size: O(n1) [2·z]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: main
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 4 + 5·z

(48) Obligation:

Complexity RNTS consisting of the following rules:

comp_f_g#1(z, z', z'') -{ 1 + z + z' }→ s' :|: s >= 0, s <= 1 * (z' - 2) + 1 * 0, s' >= 0, s' <= 1 * (z - 1) + 1 * s, z'' = 0, z - 1 >= 0, z' - 2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s'' :|: s'' >= 0, s'' <= 1 * (z - 1) + 1 * 0, z'' = 0, z' = 1 + x1 + x2, x1 >= 0, z - 1 >= 0, x2 >= 0
comp_f_g#1(z, z', z'') -{ 1 + z }→ s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * 0, z'' = 0, z - 1 >= 0, z' = 0
comp_f_g#1(z, z', z'') -{ 4 + x1' + x2' + x3' + z }→ s9 :|: s7 >= 0, s7 <= 1 * x1' + 1 * x2', s8 >= 0, s8 <= 1 * x3' + 1 * s7, s9 >= 0, s9 <= 1 * (z - 1) + 1 * s8, z'' = 0, x1' >= 0, x2' >= 0, z' = 1 + (1 + x3') + (1 + x1' + x2'), x3' >= 0, z - 1 >= 0
comp_f_g#1(z, z', z'') -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0
foldr#3(z) -{ 1 }→ 0 :|: z = 0
foldr#3(z) -{ 2 + x6 }→ 1 + x32 + s6 :|: s6 >= 0, s6 <= 1 * x6, z = 1 + x32 + x6, x32 >= 0, x6 >= 0
foldr_f#3(z, z') -{ 2 + z }→ s10 :|: s10 >= 0, s10 <= 1 * (z - 1) + 1 * 0, z' >= 0, z - 1 >= 0
foldr_f#3(z, z') -{ 5 + s5 + x16 + x32' + x6' }→ s11 :|: s11 >= 0, s11 <= 1 * x16 + 1 * (1 + x32' + s5), s5 >= 0, s5 <= 1 * x6', x6' >= 0, x32' >= 0, z' >= 0, x16 >= 0, z = 1 + x16 + (1 + x32' + x6')
foldr_f#3(z, z') -{ 1 }→ 0 :|: z = 0, z' = 0
main(z) -{ 4 }→ s12 :|: s12 >= 0, s12 <= 1 * 0, z = 0
main(z) -{ 9 + 2·s4 + 2·x16' + x6'' }→ s13 :|: s13 >= 0, s13 <= 1 * (1 + (1 + x16') + s4), s4 >= 0, s4 <= 2 * x6'', z = 1 + x16' + x6'', x6'' >= 0, x16' >= 0
map#2(z) -{ 1 }→ 0 :|: z = 0
map#2(z) -{ 2 + x6 }→ 1 + (1 + x16) + s3 :|: s3 >= 0, s3 <= 2 * x6, z = 1 + x16 + x6, x6 >= 0, x16 >= 0
plus_x#1(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
plus_x#1(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
plus_x#1(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z - 1 >= 0, z' >= 0

Function symbols to be analyzed:
Previous analysis results are:

plus_x#1: runtime: O(n1) [1 + z], size: O(n1) [z + z'] map#2: runtime: O(n1) [1 + z], size: O(n1) [2·z] foldr#3: runtime: O(n1) [1 + z], size: O(n1) [z] comp_f_g#1: runtime: O(n1) [1 + z + z'], size: O(n1) [z + z'] foldr_f#3: runtime: O(n1) [2 + 2·z], size: O(n1) [z] main: runtime: O(n1) [4 + 5·z], size: O(n1) [2·z]

(49) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(50) BOUNDS(1, n^1)